{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}

module TopLevelFunctions where

import TypeBasics (encode)
import TypeSums (inject)
import Yoko

import Common


newtype Occ = Occ (Either Int Int)
instance Show Occ where
  show (Occ (Left  i)) = '^' : show i
  show (Occ (Right i)) = show i

data TopTerm = DVar Int [Occ] | Var Occ
             | App TopTerm TopTerm deriving Show

type FunDec = ([Type], [Type], Type, TopTerm)
data TopProg = Prog [FunDec] TopTerm deriving Show





data DVar_ = DVar_ Int [Occ]
data Var_ = Var_ Occ
data App_  = App_ TopTerm TopTerm



type instance Range DVar_ = TopTerm
type instance Range Var_  = TopTerm
type instance Range App_  = TopTerm

type instance Tag DVar_ = $(return $ encode "DVar")
type instance Tag Var_ = $(return $ encode "Var")
type instance Tag App_  = $(return $ encode "App")

concat `fmap` mapM derive [''TopTerm, ''DVar_, ''Var_, ''App_]



type instance Rep DVar_ = Dep Int :*: Dep [Occ]
instance Generic DVar_ where
  rep (DVar_ i os) = Dep i :*: Dep os
  obj (Dep i :*: Dep os) = DVar_ i os
type instance Rep Var_ = Dep Occ
instance Generic Var_ where
  rep (Var_ o) = Dep o
  obj (Dep o) = Var_ o
type instance Rep App_ = Rec TopTerm :*: Rec TopTerm
instance Generic App_ where
  rep (App_ tm1 tm2) = Rec tm1 :*: Rec tm2
  obj (Rec tm1 :*: Rec tm2) = App_ tm1 tm2



type instance DCs TopTerm = (N DVar_ :+: N Var_) :+: N App_
instance DT TopTerm where
  disband (DVar i os)   = DCsOf . inject $ DVar_ i os
  disband (Var o)       = DCsOf . inject $ Var_ o
  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
instance DC DVar_ where rejoin (DVar_ i os)   = DVar i os
instance DC Var_  where rejoin (Var_  o)      = Var o
instance DC App_  where rejoin (App_ tm1 tm2) = App tm1 tm2
